dec:(KndType), ra, rt:(IdId), rainv, rtinv:(Id(Id+Unit)).
(tg1, tg2:Id. rtinv(tg2) = inl(tg1)  tg2 = rt(tg1))
 (a1, a2:Id. rainv(a2) = inl(a1)  a2 = ra(a1))
 (a:Action(dec). action-rename(rainv;rtinv;a)  Action(k.dec(kind-rename(ra;rt;k)))) 

latex

Definitions	T, True, 2of(t), , 1of(t), x. t(x), IdLnk, kind-rename(ra;rt;k), locl(a), rcv(l,tg), kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), action-rename(rainv;rtinv;a), Action(dec), x:A. B(x), P  Q, Prop, Unit, Id, Knd, t  T
Lemmas	Knd wf, Id wf, unit wf, action wf, kind-rename wf, locl wf, IdLnk wf, pi1 wf, rcv wf, it wf, true wf, squash wf